Step of Proof: eq_int_cases_test 9,38
Inference at * 1 0 2 1 
Iof proof for Lemma eq int cases test:

.....wf..... NILNIL

1. A : Type
2. x : A
3. y : A
4. P : A
5. i : 
6. j : 
7. P(if (i = j) then x else y fi )
  (i = j)   
latex
 by Id  
latex

 1: .....wf..... NILNIL

 1:   (i = j)  
 .

origin